es:ES, L:(Id List).
fischer(L)
 (e:E, j:Id.
 Newround(e)
  (j  L)
  ((j = loc(e)))
  (kind(the rcv(free message from e to j)) = rcv(<loc(e), j, "z">,"free")  Knd)) 

latex

Definitions	t.2, tag(k), outl(x), lnk(k), tt, True, if b then t else f fi , ff, eq_atom$n(x;y), Atom2Deq, IdDeq, t.1, eqof(d), , a = b, P  Q, P  Q, t  T, tag(e), lnk(e), isrcv(e), b, IdLnk, A c B, P & Q, "$x", rcv(l,tg), the rcv(free message from e1 to j), A, Newround(e), P  Q, Id, x:A. B(x), False, xL. P(x), P  Q, @i(x:T), @e(xv), fischer(L)
Lemmas	event system wf, fischer wf, es-E wf, es-when wf, es-change-to wf, Id wf, l member wf, not wf, es-loc wf, es-kind-first-from, false wf, assert-eq-id, eq id wf, assert wf, not functionality wrt iff, es-first-from wf, es-rcv-kind